<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | Main / References 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Welcome.html'>Main</a> /
</p><h1>References</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<div class="latex2html">
<DL COMPACT><DD><P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=AD94" NAME="AD94">AD94</A>
<DD>
R.&nbsp;Alur and D.&nbsp;Dill.
<BR>A theory of timed automata.
<BR><EM>Theoretical Computer Science</EM>, 126:183-235, 1994.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=AH99" NAME="AH99">AH99</A>
<DD>
R.&nbsp;Alur and T.&nbsp;Henzinger.
<BR>Reactive modules.
<BR><EM>Formal Methods in System Design</EM>, 15(1):7-48, 1999.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=ASSB96" NAME="ASSB96">ASSB96</A>
<DD>
A.&nbsp;Aziz, K.&nbsp;Sanwal, V.&nbsp;Singhal, and R.&nbsp;Brayton.
<BR>Verifying continuous time Markov chains.
<BR>In R.&nbsp;Alur and T.&nbsp;Henzinger, editors, <EM>Proc. 8th International
  Conference on Computer Aided Verification (CAV'96)</EM>, volume 1102 of <EM>  LNCS</EM>, pages 269-276. Springer, 1996.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=Bai98" NAME="Bai98">Bai98</A>
<DD>
C.&nbsp;Baier.
<BR>On algorithmic verification methods for probabilistic systems, 1998.
<BR>Habilitation thesis, Fakult&#228;t f&#252;r Mathematik &amp; Informatik,
  Universit&#228;t Mannheim.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=BKH99" NAME="BKH99">BKH99</A>
<DD>
C.&nbsp;Baier, J.-P. Katoen, and H.&nbsp;Hermanns.
<BR>Approximate symbolic model checking of continuous-time Markov
  chains.
<BR>In J.&nbsp;Baeten and S.&nbsp;Mauw, editors, <EM>Proc. 10th International
  Conference on Concurrency Theory (CONCUR'99)</EM>, volume 1664 of <EM>LNCS</EM>,
  pages 146-161. Springer, 1999.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=BK98" NAME="BK98">BK98</A>
<DD>
C.&nbsp;Baier and M.&nbsp;Kwiatkowska.
<BR>Model checking for a probabilistic branching time logic with
  fairness.
<BR><EM>Distributed Computing</EM>, 11(3):125-155, 1998.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=BdA95" NAME="BdA95">BdA95</A>
<DD>
A.&nbsp;Bianco and L.&nbsp;de&nbsp;Alfaro.
<BR>Model checking of probabilistic and nondeterministic systems.
<BR>In P.&nbsp;Thiagarajan, editor, <EM>Proc. 15th Conference on Foundations
  of Software Technology and Theoretical Computer Science (FSTTCS'95)</EM>,
  volume 1026 of <EM>LNCS</EM>, pages 499-513. Springer, 1995.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=HJ94" NAME="HJ94">HJ94</A>
<DD>
H.&nbsp;Hansson and B.&nbsp;Jonsson.
<BR>A logic for reasoning about time and reliability.
<BR><EM>Formal Aspects of Computing</EM>, 6(5):512-535, 1994.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=HLMP04" NAME="HLMP04">HLMP04</A>
<DD>
T.&nbsp;H&#233;rault, R.&nbsp;Lassaigne, F.&nbsp;Magniette, and S.&nbsp;Peyronnet.
<BR>Approximate probabilistic model checking.
<BR>In <EM>Proc. 5th International Conference on Verification, Model
  Checking and Abstract Interpretation (VMCAI'04)</EM>, volume 2937 of <EM>  LNCS</EM>, pages 307-329. Springer, 2004.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=HKN+03" NAME="HKN+03">HKN+03</A>
<DD>
H.&nbsp;Hermanns, M.&nbsp;Kwiatkowska, G.&nbsp;Norman, D.&nbsp;Parker, and M.&nbsp;Siegle.
<BR>On the use of MTBDDs for performability analysis and verification
  of stochastic systems.
<BR><EM>Journal of Logic and Algebraic Programming: Special Issue on
  Probabilistic Techniques for the Design and Analysis of Systems</EM>,
  56(1-2):23-67, 2003.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=Hil96" NAME="Hil96">Hil96</A>
<DD>
J.&nbsp;Hillston.
<BR><EM>A Compositional Approach to Performance Modelling</EM>.
<BR>Cambridge University Press, 1996.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=KSK76" NAME="KSK76">KSK76</A>
<DD>
J.&nbsp;Kemeny, J.&nbsp;Snell, and A.&nbsp;Knapp.
<BR><EM>Denumerable Markov Chains</EM>.
<BR>Springer-Verlag, 2nd edition, 1976.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=KNP04b" NAME="KNP04b">KNP04b</A>
<DD>
M.&nbsp;Kwiatkowska, G.&nbsp;Norman, and D.&nbsp;Parker.
<BR>Probabilistic symbolic model checking with PRISM: A hybrid
  approach.
<BR><EM>International Journal on Software Tools for Technology Transfer
  (STTT)</EM>, 6(2):128-142, 2004.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=KNP07a" NAME="KNP07a">KNP07a</A>
<DD>
M.&nbsp;Kwiatkowska, G.&nbsp;Norman, and D.&nbsp;Parker.
<BR>Stochastic model checking.
<BR>In M.&nbsp;Bernardo and J.&nbsp;Hillston, editors, <EM>Formal Methods for the
  Design of Computer, Communication and Software Systems: Performance
  Evaluation (SFM'07)</EM>, volume 4486 of <EM>LNCS (Tutorial Volume)</EM>, pages
  220-270. Springer, 2007.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=KNP09c" NAME="KNP09c">KNP09c</A>
<DD>
M.&nbsp;Kwiatkowska, G.&nbsp;Norman, and D.&nbsp;Parker.
<BR>Stochastic games for verification of probabilistic timed automata.
<BR>In J.&nbsp;Ouaknine and F.&nbsp;Vaandrager, editors, <EM>Proc. 7th
  International Conference on Formal Modelling and Analysis of Timed Systems
  (FORMATS'09)</EM>, volume 5813 of <EM>LNCS</EM>, pages 212-227. Springer, 2009.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=KNPS06" NAME="KNPS06">KNPS06</A>
<DD>
M.&nbsp;Kwiatkowska, G.&nbsp;Norman, D.&nbsp;Parker, and J.&nbsp;Sproston.
<BR>Performance analysis of probabilistic timed automata using digital
  clocks.
<BR><EM>Formal Methods in System Design</EM>, 29:33-78, 2006.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=KNPS08" NAME="KNPS08">KNPS08</A>
<DD>
M.&nbsp;Kwiatkowska, G.&nbsp;Norman, D.&nbsp;Parker, and J.&nbsp;Sproston.
<BR><EM>Modeling and Verification of Real-Time Systems: Formalisms and
  Software Tools</EM>, chapter Verification of Real-Time Probabilistic Systems,
  pages 249-288.
<BR>John Wiley &amp; Sons, 2008.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=Nim10" NAME="Nim10">Nim10</A>
<DD>
V.&nbsp;Nimal.
<BR><EM>Statistical Approaches for Probabilistic Model Checking</EM>.
<BR>MSc Mini-project Dissertation, Oxford University Computing
  Laboratory, 2010.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=Par02" NAME="Par02">Par02</A>
<DD>
D.&nbsp;Parker.
<BR><EM>Implementation of Symbolic Model Checking for Probabilistic
  Systems</EM>.
<BR>Ph.D. thesis, University of Birmingham, 2002.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=Seg95" NAME="Seg95">Seg95</A>
<DD>
R.&nbsp;Segala.
<BR><EM>Modelling and Verification of Randomized Distributed Real Time
  Systems</EM>.
<BR>Ph.D. thesis, Massachusetts Institute of Technology, 1995.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=Ste94" NAME="Ste94">Ste94</A>
<DD>
W.&nbsp;J. Stewart.
<BR><EM>Introduction to the Numerical Solution of Markov Chains</EM>.
<BR>Princeton, 1994.

<P></P><DT><A HREF="http://www.prismmodelchecker.org/bibitem.php?key=YS02" NAME="YS02">YS02</A>
<DD>
H.&nbsp;Younes and R.&nbsp;Simmons.
<BR>Probabilistic verification of discrete event systems using acceptance
  sampling.
<BR>In E.&nbsp;Brinksma and K.&nbsp;Larsen, editors, <EM>Proc. 14th International
  Conference on Computer Aided Verification (CAV'02)</EM>, volume 2404 of <EM>  LNCS</EM>, pages 223-235. Springer, 2002.
</DL>
</div>

</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='Welcome.html'>PRISM Manual</a></h3>
<ul><li><a class='wikilink' href='Contents.html'>Contents</a>
</li><li><a class='wikilink' href='Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='../InstallingPRISM/Instructions.html'>Installing PRISM</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Introduction.html'>The PRISM Language</a>
</li><li><a class='wikilink' href='../PropertySpecification/Introduction.html'>Property Specification</a>
</li><li><a class='wikilink' href='../RunningPRISM/StartingPRISM.html'>Running PRISM</a>
</li><li><a class='wikilink' href='../ConfiguringPRISM/Introduction.html'>Configuring PRISM</a>
</li><li><a class='selflink' href='References.html'>References</a>
</li><li><a class='wikilink' href='../FrequentlyAskedQuestions/Main.html'>FAQ</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
